\chapter{Conclusions and Perspectives}
\label{chap:concl}
\section{Concluding Remarks}

Expressiveness and decidability 
have been 
%largely unexplored concerns in 
little studied 
in the context of 
calculi for higher-order concurrency. 
In this dissertation we 
%have taken 
take 
a direct and minimal approach to 
%investigated 
the expressiveness and decidability 
of higher-order process calculi. %\emph{core} 
%We have focused on topics 
%which can be regarded as \emph{basic} in process calculi at large:
%. 
%These are topics that have been throughly studied in the first-order paradigm;
%however, they 
This approach finds justification in the fact that 
higher-order process calculi with 
specialized operators or modeling features often
do not admit a satisfactory interpretation into some first-order setting.
 %At this point, 
%it is unavoidable to observe that 
%As a matter of fact, 
%The results in this dissertation appears almost 20 years after the introduction of 
%Sangiorgi's representability result---probably the 
%most representative expressiveness result for higher-order process calculi.
The results in this dissertation 
concern issues which can be regarded as \emph{basic} in process calculi, namely 
(a)synchrony, polyadicity, forwarding.
As such, our contributions %can be seen to intimately related to 
might have a potential repercussion in 
the definition of a large class of higher-order process calculi.

A first achievement of our research is the introduction of 
%We have conducted our investigation with the aid of by departing from 
\hocore as a \emph{core} calculus for higher-order concurrency. 
In fact, 
\hocore provides a convenient framework to study fundamental issues of 
higher-order process calculi: it is minimal enough so as to 
%permit tractabletheoretical manipulations 
be theoretically tractable 
and, at the same time, it is expressive enough so as to 
represent interesting phenomena in higher-order concurrency. 
%Furthermore, %we find that 
%there are fragments of \hocore---such as \hof, introduced in Chapter \ref{chap:forward}---which are 
%relevant. % are decidable. 
In our opinion, \hocore can be regarded as the 
simplest, non-trivial process calculus featuring higher-order concurrency.


The most salient feature of \hocore is the \emph{absence of name passing} in communications. 
Given the prominent r\^{o}le of name passing within calculi for concurrency, 
and the fact that most known higher-order process calculi feature both name and process passing,
this could be well considered  as the main design decision in our research. 
The absence of name passing is necessary to isolate 
the behavior associated to 
process passing; as such, 
it allows to obtain more accurate assessments of the 
expressiveness of the process-passing paradigm.
In this sense, the results in this dissertation not only
deepen our understanding of process-passing communication but 
they can 
also 
be interpreted as
%provide 
indirect evidence of
the expressiveness and significance of the name-passing communication discipline.

It is worth observing that even in the absence of name passing, 
process-passing is a very expressive paradigm.
This is demonstrated by the fact that \hocore, 
\hof (the fragment of \hocore with limited forwarding), 
and \hopf (the extension of \hof with passivation)
are all shown to be Turing complete by exhibiting encodings of Minsky machines. 
%It is worth recalling that 
Remarkably, 
\hocore and its variants do not have operators for infinite behavior.
All the encodings of Minsky machines presented in this dissertation are compact and intuitive, and exploit 
convenient modelling idioms ---such as 
input-guarded replication and disjoint sum--- 
which can be expressed succinctly with process-passing only (see Chapters \ref{chap:core} and \ref{chap:forward}). 
Another result on the expressive power of process-passing 
presented in the dissertation
is the encoding of synchronous into asynchronous communication
presented in Chapter \ref{chap:separa} for \rhocore, the extension of  \hocore 
with restriction and polyadic communication.


Closely related to the absence of name passing is the treatment of \emph{restriction}. 
Restriction is a practically important construct, as it 
provides a way of enforcing modelling principles such as encapsulation and abstraction into specifications. 
Along the dissertation, the absence/presence of restriction has 
shown to have a notable influence on our developments.
The absence of restriction makes \hocore a \emph{public} calculus in which 
behavior is completely exposed; 
in Chapter \ref{chap:bt} we use this  
to show that Input-Output bisimilarity characterizes $\tau$ actions, 
a necessary step in showing decidability of
strong bisimilarity. Also, the absence of restriction was useful when 
deriving an axiomatization of strong bisimilarity, as it allowed to adapt previous results
by \cite{Moller88}, \cite{MM93}, and \cite{Hir07} for (first-order) calculi without restriction. 
Also in Chapter \ref{chap:bt} we 
%considered extensions of our core calculi with (forms of) restriction. , we 
analyzed 
\emph{top-level restrictions}, and showed that 
when 
\hocore is extended with 
four of such restrictions 
strong bisimilarity is no longer decidable. 

%Interestingly, 
The results in Chapter \ref{chap:forward} 
are also insightful with respect to restriction. 
There, we show that in \hof %$\mathrm{CCS}_!^{\nu}$ 
termination is decidable whereas convergence is undecidable.
%In \hof the situation is the same, and 
While undecidablity of convergence is shown by exhibiting a
\emph{unfaithful} encoding of Minsky machines, 
we are able to prove decidability of termination 
by appealing the theory of well-structured transition systems.
To our knowledge, ours is the first application of such theory in the higher-order setting.
%We notice that a calculus without restriction such as 
\hof is a calculus without restriction and yet it 
has the same decidability properties of $\mathrm{CCS}_!^{\nu}$, the variant of CCS 
with restriction and replication
as the only source of infinite behavior. 
Indeed, also in 
$\mathrm{CCS}_!^{\nu}$
termination is decidable and convergence is undecidable \citep{Busi09}.
We find this surprising because
%the same proof technique that \cite{Busi09} exploit. 
%It is indeed surprising because 
it is well-known that in fragments of CCS \emph{without restriction}
decision problems such as termination and convergence of processes are decidable.\footnote{In fact,
\cite{Goltz88} has shown that the fragment of CCS without restriction and relabeling
can be translated into a strongly bisimilar finite Petri net. 
Since termination and convergence are decidable for finite Petri nets
(see, e.g., \citep{EsparzaN94})---and strong bisimilarity preserves both properties---we can conclude that both termination and convergence are decidable in such a fragment of CCS.}
%in such calculi, undecidability appears as soon as restriction is considered.
This observation on the presence of restriction also bears witness of the expressiveness of process-passing.
Furthermore, the expressiveness results for \hopf 
given in Chapter \ref{chap:forward} can be 
alternatively interpreted
from the point of view of restriction. In fact, passivation as we define it here 
adds a subtle notion of structure to higher-order processes.
This reminds us of the 
r\^{o}le of restriction in expressiveness studies for other process calculi.
In that sense, passivation can be considered 
as a very relaxed form of restriction. It is worth noticing that 
%also in Chapter \ref{chap:forward} 
the addition of passivation 
to \hof allows to describe a \emph{faithful} encoding of Minsky machines,
thus showing that both convergence and termination are undecidable in \hopf. 
The notion of structure on processes induced by passivation units 
is therefore crucial to both expressiveness and decidability of \hopf. 

Finally, in Chapter \ref{chap:separa} we consider extensions of \hocore with full (i.e., ordinary) restriction.
There, we discussed how the scope extrusion one obtains with restriction but without
name-passing is \emph{incomplete} in that (restricted) names can be passed around inside processes
but cannot be effectively used within of receiving context. 
As a result, with only process-passing it is not possible to establish \emph{private links}
as those used in encodings of synchronous and polyadic communication in first-order calculi.
This insight is central to the separation results
for \shocore (i.e., the synchronous variant of \rhocore).
By combining selected features from 
a more informative LTS and a rather demanding notion of encoding  we were able to show that
\hopis{n}{×} 
(i.e. the instance of \shocore with $n$-adic communication) 
cannot be encoded into \hopis{n-1}{×}, thus determining a \emph{hierarchy}
of higher-order process calculi based on polyadicity. 
This result suggests that in the absence of the name-passing, 
the impact of adding restriction diminishes. 
The last result in Chapter \ref{chap:separa} shows that the ability of establishing 
private links in \shocore (that is, the ability of fully exploiting restriction and restricted names)
is obtained when extending \shocore with abstraction-passing. 
This is an insightful result, in that abstraction is arguably one of the most practically useful 
constructs in the higher-order $\pi$-calculus. 


%Because of the minimal and direct approach we have followed, 
%our results complements the research done on \emph{concurrent extensions of the $\lambda$-calculus.}

%In this dissertation we do not address
%the use of the higher-order process calculi as \emph{modelling languages}. % in concrete application areas. 
%This is an issue that goes beyond the theoretical character of expressiveness studies; 
%it refers to the kind of modelling idioms that can be neatly expressed in the 
% studied in this dissertation.
%language(s) of interest. 
Along the dissertation we describe the way in which  basic modeling idioms such as 
lists, counters, and constructs for choice and guarded infinite behavior can be expressed
in core higher-order process calculi.
Nevertheless, 
this does not seem enough so as to consider 
core higher-order process calculi 
as adequate as \emph{modelling languages} in concrete application areas.
In our opinion, higher-order process calculi for specialized application areas
should arise from the careful combination of higher-order constructs and name-passing features.


\section{Ongoing and Future Work}

Along the dissertation we have already pointed out a number of strands for future work.
We conclude by commenting on those directions we find particularly promising; some of them are object of current work.

\paragraph{More on Expressiveness of Passivation.}
In Chapter \ref{chap:forward} we have examined the expressiveness associated to 
suspension operators by studying the influence a passivation operator has on the 
absolute expressive power of a higher-order process calculus with restricted output actions.
%To the best of our knowledge, ours is the first study on expressiveness of passivation-like
%operators in the higher-order setting.  
In this respect, much remains to be done. In fact, %as outlined in Chapter \ref{chap:forward},
we have considered a particular form of passivation, 
one that allows to both suspend a process and then restart it later. 
Other forms of passivation (more precisely, other semantics for passivation)
are also possible and could be %. Other forms of passivation are 
relevant. A natural concern is that, as we pointed out before, passivation as defined here has
a very non-deterministic character. It is reasonable to assume that 
the kind of passivation required for applications in dynamic system reconfiguration
to be more controlled. 

%. Making passivation more ``opaque'' so as to resemble movement in Ambients.
%Together with Cinzia Di Giusto and Gianluigi Zavattaro, the author has 
We have conducted preliminary studies on the expressiveness of 
passivation in the context of 
$\mathrm{aCCS}^{-\nu}_{!}$, 
the asynchronous fragment of CCS without restriction and with replication \citep{DiGiustoPZ-susp09}.
In the absence of process-passing
a passivation action entails essentially the \emph{destruction} of 
the content of the passivation unit. 
That is, suspension represents a ``kill'' action over a process.
We think that this ``destructive passivation'' is perhaps the simplest kind of passivation one could think of. 
In \citep{DiGiustoPZ-susp09} we show that 
even destructive passivation is enough to 
increase the expressive power 
of 
$\mathrm{aCCS}^{-\nu}_{!}$.
Using the same theoretical machinery as in Chapter \ref{chap:forward} 
(i.e. unfaithful encodings of Minsky machines
and well-structured transition systems)
%our preliminary results 
we
show that 
in $\mathrm{aCCS}^{-\nu}_{!}$ extended with passivation:
(i) in contrast to the situation in $\mathrm{aCCS}^{-\nu}_{!}$, 
convergence is undecidable; and (ii)
similarly as in $\mathrm{aCCS}^{-\nu}_{!}$, 
%in $\mathrm{aCCS}^{-\nu}_{!}$ extended with passivation
termination 
%in the extension with destructive passivation 
is decidable.

 \paragraph{Higher-Order and Ambient-like Calculi.}
Ambient-like and higher-order process calculi
%Both formalisms 
are similar in that they 
involve 
 complex  objects in interactions. 
Also, in both cases the associated behavioral theory can be hard to define, and employs similar techniques.
However, some other characteristics suggest deep differences. Communication in Ambients resembles a ``move'' operation whereas in higher-order settings it is better assimilated to a ``copy'' operation. Most notably, there is a subtle discrepancy when it comes to \emph{binding}: most (higher-order) process calculi adopt static binding only, whereas Ambient-like formalisms exhibit features of both static and dynamic binding. 

Based on the above, we find it interesting to %study the precise relationship between 
formally compare Ambient-like and higher-order calculi.
%We address this question 
From the point of view of \emph{expressiveness}, this is relevant for at least two reasons. 
First, in the light of the above differences, %independent of the result of the comparison between the formalisms, 
an encoding of Ambient calculi would represent a significant test of expressiveness for the process-passing paradigm. 
Second, it would shed light on the intrinsic nature of the Ambient primitives which have proven so successful. 

In %the short paper 
\citep{DGPerez09} we have reported on initial results of our investigation: an encoding of Ambient
calculus into a higher-order process calculi with localities 
(implemented as passivation units)
and a
form of dynamic binding. The encoding is useful to understand the nature of
Ambient communication; it also allows us to conjecture that an encoding into a
higher-order process calculus with static binding does not exist. 
%We think that i
It would be interesting to see whether this encodability result
can be exploited/strengthened so as to have a more conclusive assessment of the expressiveness of 
the higher-order paradigm with respect to the Ambient calculi. 
%In principle, 
%and based on the intricacies of the encoding, 
%aiming at an impossibility result between the two seems plausible.
Also, it is not clear how to proceed in order to 
transform our conjecture into 
%obtain 
a formal separation result.
It could be that passivation and dynamic binding
---crucial in the encoding in \citep{DGPerez09}--- 
could give hints in this case, but this remains to be explored in detail.




 \paragraph{Dimensions of Mobility.}
Together with Roland Meyer, we are studying the relationship between 
%on relating 
decidability results for the $\pi$-calculus 
and those presented in Chapter \ref{chap:forward} for \hof.
In his PhD Thesis, \cite{Meyer08} studied the notion of \emph{structural stationarity}
in the $\pi$-calculus.
Roughly speaking, structural stationarity means bounding 
 processes so as to obtain decidability results and hence perform
automatic verification techniques on them. 
In the $\pi$-calculus,  
structural stationarity arises by giving bounds 
on two \emph{dimensions} of infinite behavior:  \emph{depth} (i.e., the nesting of restrictions inside a process) 
and \emph{breadth} (i.e., the degree of parallelism of a process).
It would be 
interesting to 
determine precisely 
%study 
%what is the 
what structural stationarity means for higher-order processes, 
and its exact relationship with that in the first-order setting.
In principle, such a relationship should allow to
transfer and generalize decidability results from one setting to the other. 

% Initial results indicate that in the higher-order setting there is another dimension, called \emph{length}, 
% that should be considered as part of higher-order structural stationarity.
% Intuitively, this refers to the ability of building chains of nested input of arbitrary length, somewhat similarly
% as the implementation of counters in the encoding of Minsky machines in Section \ref{s:passiv}.
% Using Sangiorgi's encoding of higher-order $\pi$-calculus into the $\pi$-calculus, 
% we have been able to establish a surprising yet tight relationship between dimensions in 
% the higher- and the first-order setting. 
% The most interesting consequence of this relationship is that we are able to
% transfer and generalize decidability results from one setting to the other. 


 


